1: | active(nats) | → mark(adx(zeros)) | |
2: | active(zeros) | → mark(cons(0,zeros)) | |
3: | active(incr(cons(X,Y))) | → mark(cons(s(X),incr(Y))) | |
4: | active(adx(cons(X,Y))) | → mark(incr(cons(X,adx(Y)))) | |
5: | active(hd(cons(X,Y))) | → mark(X) | |
6: | active(tl(cons(X,Y))) | → mark(Y) | |
7: | active(adx(X)) | → adx(active(X)) | |
8: | active(incr(X)) | → incr(active(X)) | |
9: | active(hd(X)) | → hd(active(X)) | |
10: | active(tl(X)) | → tl(active(X)) | |
11: | adx(mark(X)) | → mark(adx(X)) | |
12: | incr(mark(X)) | → mark(incr(X)) | |
13: | hd(mark(X)) | → mark(hd(X)) | |
14: | tl(mark(X)) | → mark(tl(X)) | |
15: | proper(nats) | → ok(nats) | |
16: | proper(adx(X)) | → adx(proper(X)) | |
17: | proper(zeros) | → ok(zeros) | |
18: | proper(cons(X1,X2)) | → cons(proper(X1),proper(X2)) | |
19: | proper(0) | → ok(0) | |
20: | proper(incr(X)) | → incr(proper(X)) | |
21: | proper(s(X)) | → s(proper(X)) | |
22: | proper(hd(X)) | → hd(proper(X)) | |
23: | proper(tl(X)) | → tl(proper(X)) | |
24: | adx(ok(X)) | → ok(adx(X)) | |
25: | cons(ok(X1),ok(X2)) | → ok(cons(X1,X2)) | |
26: | incr(ok(X)) | → ok(incr(X)) | |
27: | s(ok(X)) | → ok(s(X)) | |
28: | hd(ok(X)) | → ok(hd(X)) | |
29: | tl(ok(X)) | → ok(tl(X)) | |
30: | top(mark(X)) | → top(proper(X)) | |
31: | top(ok(X)) | → top(active(X)) | |
32: | ACTIVE(nats) | → ADX(zeros) | |
33: | ACTIVE(zeros) | → CONS(0,zeros) | |
34: | ACTIVE(incr(cons(X,Y))) | → CONS(s(X),incr(Y)) | |
35: | ACTIVE(incr(cons(X,Y))) | → S(X) | |
36: | ACTIVE(incr(cons(X,Y))) | → INCR(Y) | |
37: | ACTIVE(adx(cons(X,Y))) | → INCR(cons(X,adx(Y))) | |
38: | ACTIVE(adx(cons(X,Y))) | → CONS(X,adx(Y)) | |
39: | ACTIVE(adx(cons(X,Y))) | → ADX(Y) | |
40: | ACTIVE(adx(X)) | → ADX(active(X)) | |
41: | ACTIVE(adx(X)) | → ACTIVE(X) | |
42: | ACTIVE(incr(X)) | → INCR(active(X)) | |
43: | ACTIVE(incr(X)) | → ACTIVE(X) | |
44: | ACTIVE(hd(X)) | → HD(active(X)) | |
45: | ACTIVE(hd(X)) | → ACTIVE(X) | |
46: | ACTIVE(tl(X)) | → TL(active(X)) | |
47: | ACTIVE(tl(X)) | → ACTIVE(X) | |
48: | ADX(mark(X)) | → ADX(X) | |
49: | INCR(mark(X)) | → INCR(X) | |
50: | HD(mark(X)) | → HD(X) | |
51: | TL(mark(X)) | → TL(X) | |
52: | PROPER(adx(X)) | → ADX(proper(X)) | |
53: | PROPER(adx(X)) | → PROPER(X) | |
54: | PROPER(cons(X1,X2)) | → CONS(proper(X1),proper(X2)) | |
55: | PROPER(cons(X1,X2)) | → PROPER(X1) | |
56: | PROPER(cons(X1,X2)) | → PROPER(X2) | |
57: | PROPER(incr(X)) | → INCR(proper(X)) | |
58: | PROPER(incr(X)) | → PROPER(X) | |
59: | PROPER(s(X)) | → S(proper(X)) | |
60: | PROPER(s(X)) | → PROPER(X) | |
61: | PROPER(hd(X)) | → HD(proper(X)) | |
62: | PROPER(hd(X)) | → PROPER(X) | |
63: | PROPER(tl(X)) | → TL(proper(X)) | |
64: | PROPER(tl(X)) | → PROPER(X) | |
65: | ADX(ok(X)) | → ADX(X) | |
66: | CONS(ok(X1),ok(X2)) | → CONS(X1,X2) | |
67: | INCR(ok(X)) | → INCR(X) | |
68: | S(ok(X)) | → S(X) | |
69: | HD(ok(X)) | → HD(X) | |
70: | TL(ok(X)) | → TL(X) | |
71: | TOP(mark(X)) | → TOP(proper(X)) | |
72: | TOP(mark(X)) | → PROPER(X) | |
73: | TOP(ok(X)) | → TOP(active(X)) | |
74: | TOP(ok(X)) | → ACTIVE(X) | |